Termination of the given JBC could be proven:

0 JBC
↳1 JBC2FIG (⇒)
↳2 JBCTerminationGraph
↳3 FIGtoITRSProof (⇒)
↳4 AND
    ↳5 IDP
        ↳6 IDPtoQDPProof (⇒)
        ↳7 QDP
        ↳8 UsableRulesProof (⇔)
        ↳9 QDP
        ↳10 QReductionProof (⇔)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔)
        ↳13 YES
    ↳14 IDP
        ↳15 IDPNonInfProof (⇒)
        ↳16 AND
            ↳17 IDP
                ↳18 IDependencyGraphProof (⇔)
                ↳19 TRUE
            ↳20 IDP
                ↳21 IDependencyGraphProof (⇔)
                ↳22 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: MirrorTree 
public class List {
  Tree value;
  List next;

  public List(Tree value, List next) {
    this.value = value;
    this.next = next;
  }
}


public class MirrorTree {
    public static void main(String[] args) {
		Random.args = args;
        Tree tree = Tree.createTree();

        //Now mirror the left-most path:
		mirror(tree);
    }

	public static void mirror(Tree tree) {
		Tree cur = tree;
        while (cur != null) {
            Tree t = cur.left;
            cur.left = cur.right;
            cur.right = t;
            cur = cur.right;
        }	
	}
}


public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    String string = args[index];
    index++;
    return string.length();
  }
}


public class Tree {
  Tree left;
  Tree right;
  Object value;

  public Tree(Tree l, Tree r) {
    this.left = l;
    this.right = r;
  }

  public Tree() {
  }

  public static Tree createNode() {
   if (Random.random() == 0) {
      return null;
    }
    Tree result = new Tree();
    return result;
  }

  public static Tree createTree() {
    Tree result = createNode();
    List list = new List(result, null);
    
    int counter = Random.random();
    while (counter > 0 && list != null) {
      Tree first = list.value;
      list = list.next;

      if (first != null) {
        Tree left = createNode();
        Tree right = createNode();
        first.left = left;
        first.right = right;
        list = new List(left, list);
        list = new List(right, list);
      }

      counter--;
    }

    return result;
  }

  public static void main(String[] args) {
    Random.args = args;
    createTree();
  }
}


(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
MirrorTree.main([Ljava/lang/String;)V: Graph of 49 nodes with 0 SCCs.

Tree.createTree()LTree;: Graph of 404 nodes with 1 SCC.

Tree.createNode()LTree;: Graph of 108 nodes with 0 SCCs.

MirrorTree.mirror(LTree;)V: Graph of 40 nodes with 1 SCC.


(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

Log for SCC 0:

Generated 34 rules for P and 2 rules for R.


Combined rules. Obtained 3 rules for P and 1 rules for R.


Filtered ground terms:


5566_0_mirror_Store(x1, x2) → 5566_0_mirror_Store(x2)
3787_0_mirror_NULL(x1, x2, x3) → 3787_0_mirror_NULL(x2, x3)
Tree(x1, x2, x3) → Tree(x2, x3)
3971_0_mirror_Return(x1) → 3971_0_mirror_Return

Filtered duplicate args:


3787_0_mirror_NULL(x1, x2) → 3787_0_mirror_NULL(x2)

Finished conversion. Obtained 3 rules for P and 1 rules for R. System has no predefined symbols.



Log for SCC 1:

Generated 194 rules for P and 134 rules for R.


Combined rules. Obtained 8 rules for P and 20 rules for R.


Filtered ground terms:


8486_0_createTree_LE(x1, x2, x3, x4) → 8486_0_createTree_LE(x2, x3, x4)
List(x1, x2, x3) → List(x2, x3)
Tree(x1) → Tree
Cond_8685_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_8685_1_createTree_InvokeMethod1(x1, x3, x4)
2588_0_createNode_Return(x1, x2) → 2588_0_createNode_Return
8685_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 8685_1_createTree_InvokeMethod(x1, x2, x3, x4)
Cond_8685_1_createTree_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_8685_1_createTree_InvokeMethod(x1, x3, x4)
2422_0_createNode_Return(x1, x2) → 2422_0_createNode_Return
8685_0_createNode_InvokeMethod(x1) → 8685_0_createNode_InvokeMethod
Cond_8665_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_8665_1_createTree_InvokeMethod1(x1, x3, x4)
8665_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 8665_1_createTree_InvokeMethod(x1, x2, x3, x4)
Cond_8665_1_createTree_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_8665_1_createTree_InvokeMethod(x1, x3, x4)
Cond_8486_0_createTree_LE1(x1, x2, x3, x4, x5) → Cond_8486_0_createTree_LE1(x1, x3, x4, x5)
8665_0_createNode_InvokeMethod(x1) → 8665_0_createNode_InvokeMethod
8558_0_createNode_InvokeMethod(x1) → 8558_0_createNode_InvokeMethod
Cond_8486_0_createTree_LE(x1, x2, x3, x4, x5) → Cond_8486_0_createTree_LE(x1, x3, x4, x5)
2537_0_createNode_InvokeMethod(x1, x2) → 2537_0_createNode_InvokeMethod
java.lang.ArrayIndexOutOfBoundsException(x1) → java.lang.ArrayIndexOutOfBoundsException
java.lang.IndexOutOfBoundsException(x1) → java.lang.IndexOutOfBoundsException
2226_0_random_ArrayAccess(x1, x2, x3) → 2226_0_random_ArrayAccess(x2, x3)
Cond_2376_0_createNode_NE(x1, x2, x3) → Cond_2376_0_createNode_NE(x1, x3)
2376_0_createNode_NE(x1, x2) → 2376_0_createNode_NE(x2)
2272_0_random_IntArithmetic(x1, x2, x3, x4) → 2272_0_random_IntArithmetic(x2, x3)
2667_0_createNode_InvokeMethod(x1, x2) → 2667_0_createNode_InvokeMethod
java.lang.NullPointerException(x1) → java.lang.NullPointerException
2576_0_createNode_InvokeMethod(x1, x2) → 2576_0_createNode_InvokeMethod
8752_0_createTree_InvokeMethod(x1, x2, x3, x4, x5, x6) → 8752_0_createTree_InvokeMethod(x2, x3, x4, x5)
8729_0_createTree_InvokeMethod(x1, x2, x3, x4, x5, x6) → 8729_0_createTree_InvokeMethod(x2, x3, x4, x5)
8632_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 8632_0_createTree_InvokeMethod(x2, x3, x4, x5)
8495_0_createTree_Return(x1) → 8495_0_createTree_Return
8690_0_createNode_InvokeMethod(x1, x2) → 8690_0_createNode_InvokeMethod
8672_0_createNode_InvokeMethod(x1, x2) → 8672_0_createNode_InvokeMethod

Filtered duplicate args:


8486_0_createTree_LE(x1, x2, x3) → 8486_0_createTree_LE(x1, x3)
Cond_8486_0_createTree_LE1(x1, x2, x3, x4) → Cond_8486_0_createTree_LE1(x1, x2, x4)
Cond_8486_0_createTree_LE(x1, x2, x3, x4) → Cond_8486_0_createTree_LE(x1, x2, x4)

Filtered unneeded arguments:


Cond_2376_0_createNode_NE(x1, x2) → Cond_2376_0_createNode_NE(x1)

Filtered all non-integer terms:


8486_0_createTree_LE(x1, x2) → 8486_0_createTree_LE(x2)
List(x1, x2) → List
Cond_8486_0_createTree_LE(x1, x2, x3) → Cond_8486_0_createTree_LE(x1, x3)
8558_1_createTree_InvokeMethod(x1, x2, x3, x4) → 8558_1_createTree_InvokeMethod(x1, x2, x3)
8665_1_createTree_InvokeMethod(x1, x2, x3, x4) → 8665_1_createTree_InvokeMethod(x1, x2, x3)
Cond_8486_0_createTree_LE1(x1, x2, x3) → Cond_8486_0_createTree_LE1(x1, x3)
8685_1_createTree_InvokeMethod(x1, x2, x3, x4) → 8685_1_createTree_InvokeMethod(x1, x2, x3)
8632_0_createTree_InvokeMethod(x1, x2, x3, x4) → 8632_0_createTree_InvokeMethod(x2, x3)
8729_0_createTree_InvokeMethod(x1, x2, x3, x4) → 8729_0_createTree_InvokeMethod(x2, x3)
8752_0_createTree_InvokeMethod(x1, x2, x3, x4) → 8752_0_createTree_InvokeMethod(x2, x3)
2272_0_random_IntArithmetic(x1, x2) → 2272_0_random_IntArithmetic(x2)

Filtered all free variables:


2226_0_random_ArrayAccess(x1, x2) → 2226_0_random_ArrayAccess(x1)
ARRAY(x1, x2) → ARRAY(x1)
2272_0_random_IntArithmetic(x1) → 2272_0_random_IntArithmetic
2376_0_createNode_NE(x1) → 2376_0_createNode_NE

Filtered ground terms:


Cond_2272_1_createNode_InvokeMethod1(x1, x2) → Cond_2272_1_createNode_InvokeMethod1(x1)
2272_1_createNode_InvokeMethod(x1) → 2272_1_createNode_InvokeMethod
Cond_2272_1_createNode_InvokeMethod(x1, x2) → Cond_2272_1_createNode_InvokeMethod(x1)

Combined rules. Obtained 8 rules for P and 18 rules for R.


Finished conversion. Obtained 8 rules for P and 18 rules for R. System has predefined symbols.


(4) Complex Obligation (AND)

(5) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:
none


The ITRS R consists of the following rules:
3787_0_mirror_NULL(NULL) → 3971_0_mirror_Return

The integer pair graph contains the following rules and edges:
(0): 5566_0_MIRROR_STORE(x0[0]) → 3787_0_MIRROR_NULL(x0[0])
(1): 3787_0_MIRROR_NULL(java.lang.Object(Tree(x0[1], x1[1]))) → 3787_0_MIRROR_NULL(x0[1])
(2): 3787_0_MIRROR_NULL(java.lang.Object(Tree(x0[2], x1[2]))) → 5566_0_MIRROR_STORE(x0[2])

(0) -> (1), if ((x0[0] →* java.lang.Object(Tree(x0[1], x1[1]))))


(0) -> (2), if ((x0[0] →* java.lang.Object(Tree(x0[2], x1[2]))))


(1) -> (1), if ((x0[1] →* java.lang.Object(Tree(x0[1]', x1[1]'))))


(1) -> (2), if ((x0[1] →* java.lang.Object(Tree(x0[2], x1[2]))))


(2) -> (0), if ((x0[2] →* x0[0]))



The set Q consists of the following terms:
3787_0_mirror_NULL(NULL)

(6) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

5566_0_MIRROR_STORE(x0[0]) → 3787_0_MIRROR_NULL(x0[0])
3787_0_MIRROR_NULL(java.lang.Object(Tree(x0[1], x1[1]))) → 3787_0_MIRROR_NULL(x0[1])
3787_0_MIRROR_NULL(java.lang.Object(Tree(x0[2], x1[2]))) → 5566_0_MIRROR_STORE(x0[2])

The TRS R consists of the following rules:

3787_0_mirror_NULL(NULL) → 3971_0_mirror_Return

The set Q consists of the following terms:

3787_0_mirror_NULL(NULL)

We have to consider all minimal (P,Q,R)-chains.

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

5566_0_MIRROR_STORE(x0[0]) → 3787_0_MIRROR_NULL(x0[0])
3787_0_MIRROR_NULL(java.lang.Object(Tree(x0[1], x1[1]))) → 3787_0_MIRROR_NULL(x0[1])
3787_0_MIRROR_NULL(java.lang.Object(Tree(x0[2], x1[2]))) → 5566_0_MIRROR_STORE(x0[2])

R is empty.
The set Q consists of the following terms:

3787_0_mirror_NULL(NULL)

We have to consider all minimal (P,Q,R)-chains.

(10) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

3787_0_mirror_NULL(NULL)

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

5566_0_MIRROR_STORE(x0[0]) → 3787_0_MIRROR_NULL(x0[0])
3787_0_MIRROR_NULL(java.lang.Object(Tree(x0[1], x1[1]))) → 3787_0_MIRROR_NULL(x0[1])
3787_0_MIRROR_NULL(java.lang.Object(Tree(x0[2], x1[2]))) → 5566_0_MIRROR_STORE(x0[2])

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • 3787_0_MIRROR_NULL(java.lang.Object(Tree(x0[2], x1[2]))) → 5566_0_MIRROR_STORE(x0[2])
    The graph contains the following edges 1 > 1

  • 3787_0_MIRROR_NULL(java.lang.Object(Tree(x0[1], x1[1]))) → 3787_0_MIRROR_NULL(x0[1])
    The graph contains the following edges 1 > 1

  • 5566_0_MIRROR_STORE(x0[0]) → 3787_0_MIRROR_NULL(x0[0])
    The graph contains the following edges 1 >= 1

(13) YES

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer


The ITRS R consists of the following rules:
8558_0_createNode_InvokeMethod → 8672_0_createNode_InvokeMethod
8558_0_createNode_InvokeMethod → 8690_0_createNode_InvokeMethod
8486_0_createTree_LE(0) → 8495_0_createTree_Return
8558_0_createNode_InvokeMethod → 2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0))))
8558_1_createTree_InvokeMethod(2537_0_createNode_InvokeMethod, x0, x1) → 8632_0_createTree_InvokeMethod(x0, x1)
8558_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1) → 8632_0_createTree_InvokeMethod(x0, x1)
8558_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1) → 8632_0_createTree_InvokeMethod(x0, x1)
8665_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1) → 8729_0_createTree_InvokeMethod(x0, x1)
8665_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1) → 8729_0_createTree_InvokeMethod(x0, x1)
8665_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1) → 8752_0_createTree_InvokeMethod(x0, x1)
8665_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1) → 8752_0_createTree_InvokeMethod(x0, x1)
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2576_0_createNode_InvokeMethod
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2537_0_createNode_InvokeMethod
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2667_0_createNode_InvokeMethod
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2422_0_createNode_Return
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2588_0_createNode_Return

The integer pair graph contains the following rules and edges:
(0): 8486_0_CREATETREE_LE(x2[0]) → COND_8486_0_CREATETREE_LE(x2[0] > 0, x2[0])
(1): COND_8486_0_CREATETREE_LE(TRUE, x2[1]) → 8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1])
(2): 8558_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[2], x1[2]) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[2], x1[2])
(3): 8486_0_CREATETREE_LE(x1[3]) → COND_8486_0_CREATETREE_LE1(x1[3] > 0, x1[3])
(4): COND_8486_0_CREATETREE_LE1(TRUE, x1[4]) → 8486_0_CREATETREE_LE(x1[4] + -1)
(5): 8665_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[5], x1[5]) → COND_8665_1_CREATETREE_INVOKEMETHOD(x1[5] > 0, 2422_0_createNode_Return, x0[5], x1[5])
(6): COND_8665_1_CREATETREE_INVOKEMETHOD(TRUE, 2422_0_createNode_Return, x0[6], x1[6]) → 8486_0_CREATETREE_LE(x1[6] + -1)
(7): 8665_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[7], x1[7]) → COND_8665_1_CREATETREE_INVOKEMETHOD1(x1[7] > 0, 2588_0_createNode_Return, x0[7], x1[7])
(8): COND_8665_1_CREATETREE_INVOKEMETHOD1(TRUE, 2588_0_createNode_Return, x0[8], x1[8]) → 8486_0_CREATETREE_LE(x1[8] + -1)
(9): 8558_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[9], x1[9]) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[9], x1[9])

(0) -> (1), if ((x2[0] > 0 →* TRUE)∧(x2[0] →* x2[1]))


(1) -> (2), if ((8558_0_createNode_InvokeMethod →* 2422_0_createNode_Return)∧(x1[1] →* x0[2])∧(x2[1] →* x1[2]))


(1) -> (9), if ((8558_0_createNode_InvokeMethod →* 2588_0_createNode_Return)∧(x1[1] →* x0[9])∧(x2[1] →* x1[9]))


(2) -> (5), if ((8558_0_createNode_InvokeMethod →* 2422_0_createNode_Return)∧(x0[2] →* x0[5])∧(x1[2] →* x1[5]))


(2) -> (7), if ((8558_0_createNode_InvokeMethod →* 2588_0_createNode_Return)∧(x0[2] →* x0[7])∧(x1[2] →* x1[7]))


(3) -> (4), if ((x1[3] > 0 →* TRUE)∧(x1[3] →* x1[4]))


(4) -> (0), if ((x1[4] + -1 →* x2[0]))


(4) -> (3), if ((x1[4] + -1 →* x1[3]))


(5) -> (6), if ((x1[5] > 0 →* TRUE)∧(x0[5] →* x0[6])∧(x1[5] →* x1[6]))


(6) -> (0), if ((x1[6] + -1 →* x2[0]))


(6) -> (3), if ((x1[6] + -1 →* x1[3]))


(7) -> (8), if ((x1[7] > 0 →* TRUE)∧(x0[7] →* x0[8])∧(x1[7] →* x1[8]))


(8) -> (0), if ((x1[8] + -1 →* x2[0]))


(8) -> (3), if ((x1[8] + -1 →* x1[3]))


(9) -> (5), if ((8558_0_createNode_InvokeMethod →* 2422_0_createNode_Return)∧(x0[9] →* x0[5])∧(x1[9] →* x1[5]))


(9) -> (7), if ((8558_0_createNode_InvokeMethod →* 2588_0_createNode_Return)∧(x0[9] →* x0[7])∧(x1[9] →* x1[7]))



The set Q consists of the following terms:
8558_0_createNode_InvokeMethod
8486_0_createTree_LE(0)
8558_1_createTree_InvokeMethod(2537_0_createNode_InvokeMethod, x0, x1)
8558_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1)
8558_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1)
8665_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1)
8665_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1)
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0))))

(15) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair 8486_0_CREATETREE_LE(x2) → COND_8486_0_CREATETREE_LE(>(x2, 0), x2) the following chains were created:
  • We consider the chain 8486_0_CREATETREE_LE(x2[0]) → COND_8486_0_CREATETREE_LE(>(x2[0], 0), x2[0]), COND_8486_0_CREATETREE_LE(TRUE, x2[1]) → 8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1]) which results in the following constraint:

    (1)    (>(x2[0], 0)=TRUE∧x2[0]=x2[1] ⇒ 8486_0_CREATETREE_LE(x2[0])≥NonInfC∧8486_0_CREATETREE_LE(x2[0])≥COND_8486_0_CREATETREE_LE(>(x2[0], 0), x2[0])∧(UIncreasing(COND_8486_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥))



    We simplified constraint (1) using rule (IV) which results in the following new constraint:

    (2)    (>(x2[0], 0)=TRUE ⇒ 8486_0_CREATETREE_LE(x2[0])≥NonInfC∧8486_0_CREATETREE_LE(x2[0])≥COND_8486_0_CREATETREE_LE(>(x2[0], 0), x2[0])∧(UIncreasing(COND_8486_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (x2[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_8486_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥)∧[(2)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]x2[0] ≥ 0∧[1 + (-1)bso_38] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (x2[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_8486_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥)∧[(2)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]x2[0] ≥ 0∧[1 + (-1)bso_38] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (x2[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_8486_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥)∧[(2)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]x2[0] ≥ 0∧[1 + (-1)bso_38] ≥ 0)



    We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (6)    (x2[0] ≥ 0 ⇒ (UIncreasing(COND_8486_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥)∧[(4)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]x2[0] ≥ 0∧[1 + (-1)bso_38] ≥ 0)







For Pair COND_8486_0_CREATETREE_LE(TRUE, x2) → 8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1, x2) the following chains were created:
  • We consider the chain COND_8486_0_CREATETREE_LE(TRUE, x2[1]) → 8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1]) which results in the following constraint:

    (7)    (COND_8486_0_CREATETREE_LE(TRUE, x2[1])≥NonInfC∧COND_8486_0_CREATETREE_LE(TRUE, x2[1])≥8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1])∧(UIncreasing(8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1])), ≥))



    We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (8)    ((UIncreasing(8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1])), ≥)∧[(-1)bso_40] ≥ 0)



    We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (9)    ((UIncreasing(8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1])), ≥)∧[(-1)bso_40] ≥ 0)



    We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (10)    ((UIncreasing(8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1])), ≥)∧[(-1)bso_40] ≥ 0)



    We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (11)    ((UIncreasing(8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1])), ≥)∧0 = 0∧[(-1)bso_40] ≥ 0)







For Pair 8558_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0, x1) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0, x1) the following chains were created:
  • We consider the chain 8558_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[2], x1[2]) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[2], x1[2]) which results in the following constraint:

    (12)    (8558_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[2], x1[2])≥NonInfC∧8558_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[2], x1[2])≥8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[2], x1[2])∧(UIncreasing(8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[2], x1[2])), ≥))



    We simplified constraint (12) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (13)    ((UIncreasing(8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[2], x1[2])), ≥)∧[(-1)bso_42] ≥ 0)



    We simplified constraint (13) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (14)    ((UIncreasing(8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[2], x1[2])), ≥)∧[(-1)bso_42] ≥ 0)



    We simplified constraint (14) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (15)    ((UIncreasing(8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[2], x1[2])), ≥)∧[(-1)bso_42] ≥ 0)



    We simplified constraint (15) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (16)    ((UIncreasing(8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[2], x1[2])), ≥)∧0 = 0∧[(-1)bso_42] ≥ 0)







For Pair 8486_0_CREATETREE_LE(x1) → COND_8486_0_CREATETREE_LE1(>(x1, 0), x1) the following chains were created:
  • We consider the chain 8486_0_CREATETREE_LE(x1[3]) → COND_8486_0_CREATETREE_LE1(>(x1[3], 0), x1[3]), COND_8486_0_CREATETREE_LE1(TRUE, x1[4]) → 8486_0_CREATETREE_LE(+(x1[4], -1)) which results in the following constraint:

    (17)    (>(x1[3], 0)=TRUE∧x1[3]=x1[4] ⇒ 8486_0_CREATETREE_LE(x1[3])≥NonInfC∧8486_0_CREATETREE_LE(x1[3])≥COND_8486_0_CREATETREE_LE1(>(x1[3], 0), x1[3])∧(UIncreasing(COND_8486_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥))



    We simplified constraint (17) using rule (IV) which results in the following new constraint:

    (18)    (>(x1[3], 0)=TRUE ⇒ 8486_0_CREATETREE_LE(x1[3])≥NonInfC∧8486_0_CREATETREE_LE(x1[3])≥COND_8486_0_CREATETREE_LE1(>(x1[3], 0), x1[3])∧(UIncreasing(COND_8486_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥))



    We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (19)    (x1[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_8486_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥)∧[(2)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]x1[3] ≥ 0∧[2 + (-1)bso_44] ≥ 0)



    We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (20)    (x1[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_8486_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥)∧[(2)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]x1[3] ≥ 0∧[2 + (-1)bso_44] ≥ 0)



    We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (21)    (x1[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_8486_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥)∧[(2)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]x1[3] ≥ 0∧[2 + (-1)bso_44] ≥ 0)



    We simplified constraint (21) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (22)    (x1[3] ≥ 0 ⇒ (UIncreasing(COND_8486_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥)∧[(4)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]x1[3] ≥ 0∧[2 + (-1)bso_44] ≥ 0)







For Pair COND_8486_0_CREATETREE_LE1(TRUE, x1) → 8486_0_CREATETREE_LE(+(x1, -1)) the following chains were created:
  • We consider the chain COND_8486_0_CREATETREE_LE1(TRUE, x1[4]) → 8486_0_CREATETREE_LE(+(x1[4], -1)) which results in the following constraint:

    (23)    (COND_8486_0_CREATETREE_LE1(TRUE, x1[4])≥NonInfC∧COND_8486_0_CREATETREE_LE1(TRUE, x1[4])≥8486_0_CREATETREE_LE(+(x1[4], -1))∧(UIncreasing(8486_0_CREATETREE_LE(+(x1[4], -1))), ≥))



    We simplified constraint (23) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (24)    ((UIncreasing(8486_0_CREATETREE_LE(+(x1[4], -1))), ≥)∧[(-1)bso_46] ≥ 0)



    We simplified constraint (24) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (25)    ((UIncreasing(8486_0_CREATETREE_LE(+(x1[4], -1))), ≥)∧[(-1)bso_46] ≥ 0)



    We simplified constraint (25) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (26)    ((UIncreasing(8486_0_CREATETREE_LE(+(x1[4], -1))), ≥)∧[(-1)bso_46] ≥ 0)



    We simplified constraint (26) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (27)    ((UIncreasing(8486_0_CREATETREE_LE(+(x1[4], -1))), ≥)∧0 = 0∧[(-1)bso_46] ≥ 0)







For Pair 8665_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0, x1) → COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1, 0), 2422_0_createNode_Return, x0, x1) the following chains were created:
  • We consider the chain 8665_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[5], x1[5]) → COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 2422_0_createNode_Return, x0[5], x1[5]), COND_8665_1_CREATETREE_INVOKEMETHOD(TRUE, 2422_0_createNode_Return, x0[6], x1[6]) → 8486_0_CREATETREE_LE(+(x1[6], -1)) which results in the following constraint:

    (28)    (>(x1[5], 0)=TRUE∧x0[5]=x0[6]∧x1[5]=x1[6] ⇒ 8665_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[5], x1[5])≥NonInfC∧8665_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[5], x1[5])≥COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 2422_0_createNode_Return, x0[5], x1[5])∧(UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 2422_0_createNode_Return, x0[5], x1[5])), ≥))



    We simplified constraint (28) using rule (IV) which results in the following new constraint:

    (29)    (>(x1[5], 0)=TRUE ⇒ 8665_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[5], x1[5])≥NonInfC∧8665_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[5], x1[5])≥COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 2422_0_createNode_Return, x0[5], x1[5])∧(UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 2422_0_createNode_Return, x0[5], x1[5])), ≥))



    We simplified constraint (29) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (30)    (x1[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 2422_0_createNode_Return, x0[5], x1[5])), ≥)∧[bni_47 + (-1)Bound*bni_47] + [(2)bni_47]x1[5] ≥ 0∧[(-1)bso_48] ≥ 0)



    We simplified constraint (30) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (31)    (x1[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 2422_0_createNode_Return, x0[5], x1[5])), ≥)∧[bni_47 + (-1)Bound*bni_47] + [(2)bni_47]x1[5] ≥ 0∧[(-1)bso_48] ≥ 0)



    We simplified constraint (31) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (32)    (x1[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 2422_0_createNode_Return, x0[5], x1[5])), ≥)∧[bni_47 + (-1)Bound*bni_47] + [(2)bni_47]x1[5] ≥ 0∧[(-1)bso_48] ≥ 0)



    We simplified constraint (32) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (33)    (x1[5] ≥ 0 ⇒ (UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 2422_0_createNode_Return, x0[5], x1[5])), ≥)∧[(3)bni_47 + (-1)Bound*bni_47] + [(2)bni_47]x1[5] ≥ 0∧[(-1)bso_48] ≥ 0)







For Pair COND_8665_1_CREATETREE_INVOKEMETHOD(TRUE, 2422_0_createNode_Return, x0, x1) → 8486_0_CREATETREE_LE(+(x1, -1)) the following chains were created:
  • We consider the chain COND_8665_1_CREATETREE_INVOKEMETHOD(TRUE, 2422_0_createNode_Return, x0[6], x1[6]) → 8486_0_CREATETREE_LE(+(x1[6], -1)) which results in the following constraint:

    (34)    (COND_8665_1_CREATETREE_INVOKEMETHOD(TRUE, 2422_0_createNode_Return, x0[6], x1[6])≥NonInfC∧COND_8665_1_CREATETREE_INVOKEMETHOD(TRUE, 2422_0_createNode_Return, x0[6], x1[6])≥8486_0_CREATETREE_LE(+(x1[6], -1))∧(UIncreasing(8486_0_CREATETREE_LE(+(x1[6], -1))), ≥))



    We simplified constraint (34) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (35)    ((UIncreasing(8486_0_CREATETREE_LE(+(x1[6], -1))), ≥)∧[1 + (-1)bso_50] ≥ 0)



    We simplified constraint (35) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (36)    ((UIncreasing(8486_0_CREATETREE_LE(+(x1[6], -1))), ≥)∧[1 + (-1)bso_50] ≥ 0)



    We simplified constraint (36) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (37)    ((UIncreasing(8486_0_CREATETREE_LE(+(x1[6], -1))), ≥)∧[1 + (-1)bso_50] ≥ 0)



    We simplified constraint (37) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (38)    ((UIncreasing(8486_0_CREATETREE_LE(+(x1[6], -1))), ≥)∧0 = 0∧[1 + (-1)bso_50] ≥ 0)







For Pair 8665_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0, x1) → COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1, 0), 2588_0_createNode_Return, x0, x1) the following chains were created:
  • We consider the chain 8665_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[7], x1[7]) → COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 2588_0_createNode_Return, x0[7], x1[7]), COND_8665_1_CREATETREE_INVOKEMETHOD1(TRUE, 2588_0_createNode_Return, x0[8], x1[8]) → 8486_0_CREATETREE_LE(+(x1[8], -1)) which results in the following constraint:

    (39)    (>(x1[7], 0)=TRUE∧x0[7]=x0[8]∧x1[7]=x1[8] ⇒ 8665_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[7], x1[7])≥NonInfC∧8665_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[7], x1[7])≥COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 2588_0_createNode_Return, x0[7], x1[7])∧(UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 2588_0_createNode_Return, x0[7], x1[7])), ≥))



    We simplified constraint (39) using rule (IV) which results in the following new constraint:

    (40)    (>(x1[7], 0)=TRUE ⇒ 8665_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[7], x1[7])≥NonInfC∧8665_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[7], x1[7])≥COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 2588_0_createNode_Return, x0[7], x1[7])∧(UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 2588_0_createNode_Return, x0[7], x1[7])), ≥))



    We simplified constraint (40) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (41)    (x1[7] + [-1] ≥ 0 ⇒ (UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 2588_0_createNode_Return, x0[7], x1[7])), ≥)∧[bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x1[7] ≥ 0∧[1 + (-1)bso_52] ≥ 0)



    We simplified constraint (41) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (42)    (x1[7] + [-1] ≥ 0 ⇒ (UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 2588_0_createNode_Return, x0[7], x1[7])), ≥)∧[bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x1[7] ≥ 0∧[1 + (-1)bso_52] ≥ 0)



    We simplified constraint (42) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (43)    (x1[7] + [-1] ≥ 0 ⇒ (UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 2588_0_createNode_Return, x0[7], x1[7])), ≥)∧[bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x1[7] ≥ 0∧[1 + (-1)bso_52] ≥ 0)



    We simplified constraint (43) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (44)    (x1[7] ≥ 0 ⇒ (UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 2588_0_createNode_Return, x0[7], x1[7])), ≥)∧[(3)bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x1[7] ≥ 0∧[1 + (-1)bso_52] ≥ 0)







For Pair COND_8665_1_CREATETREE_INVOKEMETHOD1(TRUE, 2588_0_createNode_Return, x0, x1) → 8486_0_CREATETREE_LE(+(x1, -1)) the following chains were created:
  • We consider the chain COND_8665_1_CREATETREE_INVOKEMETHOD1(TRUE, 2588_0_createNode_Return, x0[8], x1[8]) → 8486_0_CREATETREE_LE(+(x1[8], -1)) which results in the following constraint:

    (45)    (COND_8665_1_CREATETREE_INVOKEMETHOD1(TRUE, 2588_0_createNode_Return, x0[8], x1[8])≥NonInfC∧COND_8665_1_CREATETREE_INVOKEMETHOD1(TRUE, 2588_0_createNode_Return, x0[8], x1[8])≥8486_0_CREATETREE_LE(+(x1[8], -1))∧(UIncreasing(8486_0_CREATETREE_LE(+(x1[8], -1))), ≥))



    We simplified constraint (45) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (46)    ((UIncreasing(8486_0_CREATETREE_LE(+(x1[8], -1))), ≥)∧[(-1)bso_54] ≥ 0)



    We simplified constraint (46) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (47)    ((UIncreasing(8486_0_CREATETREE_LE(+(x1[8], -1))), ≥)∧[(-1)bso_54] ≥ 0)



    We simplified constraint (47) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (48)    ((UIncreasing(8486_0_CREATETREE_LE(+(x1[8], -1))), ≥)∧[(-1)bso_54] ≥ 0)



    We simplified constraint (48) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (49)    ((UIncreasing(8486_0_CREATETREE_LE(+(x1[8], -1))), ≥)∧0 = 0∧[(-1)bso_54] ≥ 0)







For Pair 8558_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0, x1) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0, x1) the following chains were created:
  • We consider the chain 8558_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[9], x1[9]) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[9], x1[9]) which results in the following constraint:

    (50)    (8558_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[9], x1[9])≥NonInfC∧8558_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[9], x1[9])≥8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[9], x1[9])∧(UIncreasing(8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[9], x1[9])), ≥))



    We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (51)    ((UIncreasing(8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[9], x1[9])), ≥)∧[(-1)bso_56] ≥ 0)



    We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (52)    ((UIncreasing(8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[9], x1[9])), ≥)∧[(-1)bso_56] ≥ 0)



    We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (53)    ((UIncreasing(8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[9], x1[9])), ≥)∧[(-1)bso_56] ≥ 0)



    We simplified constraint (53) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (54)    ((UIncreasing(8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[9], x1[9])), ≥)∧0 = 0∧[(-1)bso_56] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • 8486_0_CREATETREE_LE(x2) → COND_8486_0_CREATETREE_LE(>(x2, 0), x2)
    • (x2[0] ≥ 0 ⇒ (UIncreasing(COND_8486_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥)∧[(4)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]x2[0] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

  • COND_8486_0_CREATETREE_LE(TRUE, x2) → 8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1, x2)
    • ((UIncreasing(8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1])), ≥)∧0 = 0∧[(-1)bso_40] ≥ 0)

  • 8558_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0, x1) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0, x1)
    • ((UIncreasing(8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[2], x1[2])), ≥)∧0 = 0∧[(-1)bso_42] ≥ 0)

  • 8486_0_CREATETREE_LE(x1) → COND_8486_0_CREATETREE_LE1(>(x1, 0), x1)
    • (x1[3] ≥ 0 ⇒ (UIncreasing(COND_8486_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥)∧[(4)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]x1[3] ≥ 0∧[2 + (-1)bso_44] ≥ 0)

  • COND_8486_0_CREATETREE_LE1(TRUE, x1) → 8486_0_CREATETREE_LE(+(x1, -1))
    • ((UIncreasing(8486_0_CREATETREE_LE(+(x1[4], -1))), ≥)∧0 = 0∧[(-1)bso_46] ≥ 0)

  • 8665_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0, x1) → COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1, 0), 2422_0_createNode_Return, x0, x1)
    • (x1[5] ≥ 0 ⇒ (UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 2422_0_createNode_Return, x0[5], x1[5])), ≥)∧[(3)bni_47 + (-1)Bound*bni_47] + [(2)bni_47]x1[5] ≥ 0∧[(-1)bso_48] ≥ 0)

  • COND_8665_1_CREATETREE_INVOKEMETHOD(TRUE, 2422_0_createNode_Return, x0, x1) → 8486_0_CREATETREE_LE(+(x1, -1))
    • ((UIncreasing(8486_0_CREATETREE_LE(+(x1[6], -1))), ≥)∧0 = 0∧[1 + (-1)bso_50] ≥ 0)

  • 8665_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0, x1) → COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1, 0), 2588_0_createNode_Return, x0, x1)
    • (x1[7] ≥ 0 ⇒ (UIncreasing(COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 2588_0_createNode_Return, x0[7], x1[7])), ≥)∧[(3)bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x1[7] ≥ 0∧[1 + (-1)bso_52] ≥ 0)

  • COND_8665_1_CREATETREE_INVOKEMETHOD1(TRUE, 2588_0_createNode_Return, x0, x1) → 8486_0_CREATETREE_LE(+(x1, -1))
    • ((UIncreasing(8486_0_CREATETREE_LE(+(x1[8], -1))), ≥)∧0 = 0∧[(-1)bso_54] ≥ 0)

  • 8558_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0, x1) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0, x1)
    • ((UIncreasing(8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[9], x1[9])), ≥)∧0 = 0∧[(-1)bso_56] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(8558_0_createNode_InvokeMethod) = [-1]   
POL(8672_0_createNode_InvokeMethod) = [-1]   
POL(8690_0_createNode_InvokeMethod) = [-1]   
POL(8486_0_createTree_LE(x1)) = [-1]   
POL(0) = 0   
POL(8495_0_createTree_Return) = [-1]   
POL(2226_1_createNode_InvokeMethod(x1)) = [-1]   
POL(2226_0_random_ArrayAccess(x1)) = [-1]   
POL(java.lang.Object(x1)) = [-1]   
POL(ARRAY(x1)) = [-1]   
POL(8558_1_createTree_InvokeMethod(x1, x2, x3)) = [-1]   
POL(2537_0_createNode_InvokeMethod) = [-1]   
POL(8632_0_createTree_InvokeMethod(x1, x2)) = [-1]   
POL(2576_0_createNode_InvokeMethod) = [-1]   
POL(2667_0_createNode_InvokeMethod) = [-1]   
POL(8665_1_createTree_InvokeMethod(x1, x2, x3)) = [-1]   
POL(8729_0_createTree_InvokeMethod(x1, x2)) = [-1]   
POL(8752_0_createTree_InvokeMethod(x1, x2)) = [-1]   
POL(2422_0_createNode_Return) = [-1]   
POL(2588_0_createNode_Return) = [-1]   
POL(8486_0_CREATETREE_LE(x1)) = [2] + [2]x1   
POL(COND_8486_0_CREATETREE_LE(x1, x2)) = [1] + [2]x2   
POL(>(x1, x2)) = [-1]   
POL(8558_1_CREATETREE_INVOKEMETHOD(x1, x2, x3)) = [1] + [2]x3   
POL(8665_1_CREATETREE_INVOKEMETHOD(x1, x2, x3)) = [1] + [2]x3   
POL(COND_8486_0_CREATETREE_LE1(x1, x2)) = [2]x2   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(COND_8665_1_CREATETREE_INVOKEMETHOD(x1, x2, x3, x4)) = [1] + [2]x4   
POL(COND_8665_1_CREATETREE_INVOKEMETHOD1(x1, x2, x3, x4)) = [2]x4   

The following pairs are in P>:

8486_0_CREATETREE_LE(x2[0]) → COND_8486_0_CREATETREE_LE(>(x2[0], 0), x2[0])
8486_0_CREATETREE_LE(x1[3]) → COND_8486_0_CREATETREE_LE1(>(x1[3], 0), x1[3])
COND_8665_1_CREATETREE_INVOKEMETHOD(TRUE, 2422_0_createNode_Return, x0[6], x1[6]) → 8486_0_CREATETREE_LE(+(x1[6], -1))
8665_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[7], x1[7]) → COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 2588_0_createNode_Return, x0[7], x1[7])

The following pairs are in Pbound:

8486_0_CREATETREE_LE(x2[0]) → COND_8486_0_CREATETREE_LE(>(x2[0], 0), x2[0])
8486_0_CREATETREE_LE(x1[3]) → COND_8486_0_CREATETREE_LE1(>(x1[3], 0), x1[3])
8665_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[5], x1[5]) → COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 2422_0_createNode_Return, x0[5], x1[5])
8665_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[7], x1[7]) → COND_8665_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 2588_0_createNode_Return, x0[7], x1[7])

The following pairs are in P≥:

COND_8486_0_CREATETREE_LE(TRUE, x2[1]) → 8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1])
8558_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[2], x1[2]) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[2], x1[2])
COND_8486_0_CREATETREE_LE1(TRUE, x1[4]) → 8486_0_CREATETREE_LE(+(x1[4], -1))
8665_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[5], x1[5]) → COND_8665_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 2422_0_createNode_Return, x0[5], x1[5])
COND_8665_1_CREATETREE_INVOKEMETHOD1(TRUE, 2588_0_createNode_Return, x0[8], x1[8]) → 8486_0_CREATETREE_LE(+(x1[8], -1))
8558_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[9], x1[9]) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[9], x1[9])

There are no usable rules.

(16) Complex Obligation (AND)

(17) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer


The ITRS R consists of the following rules:
8558_0_createNode_InvokeMethod → 8672_0_createNode_InvokeMethod
8558_0_createNode_InvokeMethod → 8690_0_createNode_InvokeMethod
8486_0_createTree_LE(0) → 8495_0_createTree_Return
8558_0_createNode_InvokeMethod → 2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0))))
8558_1_createTree_InvokeMethod(2537_0_createNode_InvokeMethod, x0, x1) → 8632_0_createTree_InvokeMethod(x0, x1)
8558_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1) → 8632_0_createTree_InvokeMethod(x0, x1)
8558_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1) → 8632_0_createTree_InvokeMethod(x0, x1)
8665_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1) → 8729_0_createTree_InvokeMethod(x0, x1)
8665_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1) → 8729_0_createTree_InvokeMethod(x0, x1)
8665_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1) → 8752_0_createTree_InvokeMethod(x0, x1)
8665_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1) → 8752_0_createTree_InvokeMethod(x0, x1)
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2576_0_createNode_InvokeMethod
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2537_0_createNode_InvokeMethod
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2667_0_createNode_InvokeMethod
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2422_0_createNode_Return
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2588_0_createNode_Return

The integer pair graph contains the following rules and edges:
(1): COND_8486_0_CREATETREE_LE(TRUE, x2[1]) → 8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1])
(2): 8558_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[2], x1[2]) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[2], x1[2])
(4): COND_8486_0_CREATETREE_LE1(TRUE, x1[4]) → 8486_0_CREATETREE_LE(x1[4] + -1)
(5): 8665_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[5], x1[5]) → COND_8665_1_CREATETREE_INVOKEMETHOD(x1[5] > 0, 2422_0_createNode_Return, x0[5], x1[5])
(8): COND_8665_1_CREATETREE_INVOKEMETHOD1(TRUE, 2588_0_createNode_Return, x0[8], x1[8]) → 8486_0_CREATETREE_LE(x1[8] + -1)
(9): 8558_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[9], x1[9]) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[9], x1[9])

(1) -> (2), if ((8558_0_createNode_InvokeMethod →* 2422_0_createNode_Return)∧(x1[1] →* x0[2])∧(x2[1] →* x1[2]))


(2) -> (5), if ((8558_0_createNode_InvokeMethod →* 2422_0_createNode_Return)∧(x0[2] →* x0[5])∧(x1[2] →* x1[5]))


(9) -> (5), if ((8558_0_createNode_InvokeMethod →* 2422_0_createNode_Return)∧(x0[9] →* x0[5])∧(x1[9] →* x1[5]))


(1) -> (9), if ((8558_0_createNode_InvokeMethod →* 2588_0_createNode_Return)∧(x1[1] →* x0[9])∧(x2[1] →* x1[9]))



The set Q consists of the following terms:
8558_0_createNode_InvokeMethod
8486_0_createTree_LE(0)
8558_1_createTree_InvokeMethod(2537_0_createNode_InvokeMethod, x0, x1)
8558_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1)
8558_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1)
8665_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1)
8665_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1)
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0))))

(18) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 6 less nodes.

(19) TRUE

(20) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer


The ITRS R consists of the following rules:
8558_0_createNode_InvokeMethod → 8672_0_createNode_InvokeMethod
8558_0_createNode_InvokeMethod → 8690_0_createNode_InvokeMethod
8486_0_createTree_LE(0) → 8495_0_createTree_Return
8558_0_createNode_InvokeMethod → 2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0))))
8558_1_createTree_InvokeMethod(2537_0_createNode_InvokeMethod, x0, x1) → 8632_0_createTree_InvokeMethod(x0, x1)
8558_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1) → 8632_0_createTree_InvokeMethod(x0, x1)
8558_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1) → 8632_0_createTree_InvokeMethod(x0, x1)
8665_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1) → 8729_0_createTree_InvokeMethod(x0, x1)
8665_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1) → 8729_0_createTree_InvokeMethod(x0, x1)
8665_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1) → 8752_0_createTree_InvokeMethod(x0, x1)
8665_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1) → 8752_0_createTree_InvokeMethod(x0, x1)
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2576_0_createNode_InvokeMethod
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2537_0_createNode_InvokeMethod
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2667_0_createNode_InvokeMethod
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2422_0_createNode_Return
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 2588_0_createNode_Return

The integer pair graph contains the following rules and edges:
(1): COND_8486_0_CREATETREE_LE(TRUE, x2[1]) → 8558_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x1[1], x2[1])
(2): 8558_1_CREATETREE_INVOKEMETHOD(2422_0_createNode_Return, x0[2], x1[2]) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[2], x1[2])
(4): COND_8486_0_CREATETREE_LE1(TRUE, x1[4]) → 8486_0_CREATETREE_LE(x1[4] + -1)
(6): COND_8665_1_CREATETREE_INVOKEMETHOD(TRUE, 2422_0_createNode_Return, x0[6], x1[6]) → 8486_0_CREATETREE_LE(x1[6] + -1)
(8): COND_8665_1_CREATETREE_INVOKEMETHOD1(TRUE, 2588_0_createNode_Return, x0[8], x1[8]) → 8486_0_CREATETREE_LE(x1[8] + -1)
(9): 8558_1_CREATETREE_INVOKEMETHOD(2588_0_createNode_Return, x0[9], x1[9]) → 8665_1_CREATETREE_INVOKEMETHOD(8558_0_createNode_InvokeMethod, x0[9], x1[9])

(1) -> (2), if ((8558_0_createNode_InvokeMethod →* 2422_0_createNode_Return)∧(x1[1] →* x0[2])∧(x2[1] →* x1[2]))


(1) -> (9), if ((8558_0_createNode_InvokeMethod →* 2588_0_createNode_Return)∧(x1[1] →* x0[9])∧(x2[1] →* x1[9]))



The set Q consists of the following terms:
8558_0_createNode_InvokeMethod
8486_0_createTree_LE(0)
8558_1_createTree_InvokeMethod(2537_0_createNode_InvokeMethod, x0, x1)
8558_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1)
8558_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1)
8665_1_createTree_InvokeMethod(2576_0_createNode_InvokeMethod, x0, x1)
8665_1_createTree_InvokeMethod(2667_0_createNode_InvokeMethod, x0, x1)
2226_1_createNode_InvokeMethod(2226_0_random_ArrayAccess(java.lang.Object(ARRAY(x0))))

(21) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 6 less nodes.

(22) TRUE